Cmd:Type, x:chain_sys(Cmd). (csupdate?(x))  (csupdate-cmds(x)  (Cmd List)) 

latex

Definitions	if b then t else f fi , tt, ff, csupdate-cmds(x), t  T, csupdate?(x), b, P  Q, x:A. B(x), False, chain_sys(Cmd), csupdate(from;cmds), , csinput(cmd)
Lemmas	chain sys wf, csupdate? wf, assert wf, true wf, false wf